ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da).
ecl-kinds(x) = ecl-trans-ks(ecl-trans(x))  Knd List 

latex

Definitions	x:A. B(x), ecl-kinds(x), ecl-trans(x), Prop, P  Q, t  T, x. t(x), ecl-trans-ks(v), ecl-base-tuple(k;test), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), combine-ecl-tuples(A;B;f;g), , AB, A, False, combine-ecl-tuples2(A;B;f;g), SQType(T), {T}, reset-ecl-tuple(A), add-ecl-act(A;m), Y, reduce(f;k;as), ecl-add-throw(A;m), ecl-add-catch(A;l), x(s), ecl-trans-tuple{i:l}(ds;da), ||as||, P  Q, P & Q
Lemmas	ecl-induction, ecl-kinds wf, ecl-trans-ks wf, ecl-trans wf, decl-state wf, ma-valtype wf, bool wf, nat wf, ecl wf, fpf wf, Knd wf, Id wf, ecl-trans-tuple wf, append wf, combine-ecl-tuples wf, bor wf, band wf, lt int wf, le wf, Knd sq, length wf1, non neg length, cons one one